\begin{tabbing}
ma{-}single{-}effect1($x$;$A$;$y$;$B$;$k$;$T$;$f$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=with declarations \+
\\[0ex]ds:$x$ : $A$ $\oplus$ $y$ : $B$
\\[0ex]da:$k$ : $T$
\\[0ex]effect of $k$(v) is $x$ := $\lambda$$s$,$v$. $f$($s$($x$),$s$($y$),$v$) s v
\-
\end{tabbing}